.NH
Temporal Logic and Hardware Specification
.NH 2
Linear Time Temporal Logic
.PP
This section briefly introduces Linear Time Temporal Logic.
In this chapter we discuss only propositional LTTL and explain
how it can be used to specify basic timing relations for synchronization parts
The next two chapters discuss first order LTTL.
More detailed discussions about temporal logic can be found in [3,7].
.PP
Temporal Logic is an extension of traditional logic that includes
several temporal
operators and addresses discrete, rather than continuous time.
Linear Time Temporal Logic has four 
temporal operators: o (next), [] (always), <> (sometime), and U (until).
The first three are unary operators, and the last is a binary operator.
Intuitively each has the following meanings.
.IP P 6
(without temporal operators): P is true at present.
.IP o\ P
P is true in the next state (in sequential circuits, next clock).
.IP []P
P is true at present and in all the future states.
.IP <>P
P is true at least in one state, either present or in the future,     
.IP P\ U\ Q
P is true in all states until the first state in which Q is true.
.PP
In the followings, we present the techniques for specifying hardware
in LTTL.
.NH 3
Basic Relations
.PP
This section shows how to specify the basic relations which appear in the
description of hardware in temporal logic. 
We deal only with sequential circuits, and the clock provides the unit of time.
Systems are described using system states that change with time.
.PP
first of all, properties common to all states are easily described 
with the traditional logic. Here we use the following terminology.
.KS
.IP
.nf
 ->   :IMPLY
 /\e   :AND
 ,    :AND
 \e/   :OR
 ~    :NOT
.fi
.KE
.LP
We use two different notation for conjunction for readability, but
they have same meaning.
For example, 'terminal A and B are connected' is described as follows:
.IP
 A <-> B (abbreviation for A->B/\eB->A)  (1)
.LP
This is in turn expressed in temporal logic using [] operator, that is,
.IP
 [](A <-> B),  (2)
.LP
because expressions in temporal logic with no temporal operators designate
properties that are true only at the present time.
Thus traditional logic only describes permanent properties.
The [] operator can be expressed using the U operator in the following way:
.IP
 []P = P U false.   (3)
.LP
.UL false
always means false, so P must be true in all states.
The property P held in some future time, which cannot be directly expressed
using the traditional logic, is described in temporal logic as follows:
.IP
<>P.  (4)
.LP
The <> operator is the dual of the [] operator.
.IP
<>P = ~([](~P)) (5)
.LP
Temporal precedence is described using the U operator.
For example, 'A precedes B' is expressed as follows:
.IP
~(~A U B),  (6)
.LP
because 'A precedes B' is the inverse of the case where
A continues to be false until B is true.
.PP
Next we describe the dependency among variables in 
temporal sequences. 'If the signal P is active, 
then the signal Q is active from the next instant in time' (shown in Figure (1))
is described as:
.IP
[](P -> o Q).  (7)
.LP
Also, 'If the signal P is active, 
then the signal Q is active from the next next instant in time'
(shown in Figure (2))
is described as:
.IP
[](P -> o o Q).  (8)
.LP
In the same way we can describe the property: 'if signal P is active,
then the signal Q is active after n clocks'.
.LP
The property: 'if the signal P is active, then the signal Q is active
by the next instant in time' is described as follows:
.IP
[](P -> (Q \e/ o Q)).  (9)
.LP
When we cannot exactly specify the time when Q will be active,
but can say Q will eventually be
active, the following description obtains:
.IP
[](P -> <> Q).   (10)
.LP
(10) guarantees 'if P is active, then Q is active', but 
P may be active otherwise.
If it is desired 'P becomes active if and only if on the next time
when Q is active', the following expression should be added to (7).
.IP
[](~Q -> ((o ~Q) U P))).   (11)
.LP
If the same relations as above is desired on (10), (12) should be added.
.IP
[](~Q -> ((~Q) U P)))   (12)
.LP
The basic timing relationship among signals can be described with 
(7) and (11), or (10) and (12), etc..
Also, a specification slightly different from (12): 'Until P is active,
if Q is inactive, then Q continues to be inactive'
is described as
.IP
(~Q -> (~Q U P)) U P.   (13)
.PP
With expressions of te type shown above,
we can describe various timing relations
among variables and specify the synchronization part of hardware.
.NH 3
Logic Gates
.PP
Hardware components, such as logic gates, are described in temporal
logic as follows.
first, we describe combinational gates, such as AND, OR, NOR, etc.. 
For example, an AND gate, shown in Figure (3), is described in the 
following way.
.IP
[]((A /\e B) <-> Out).  (14)
.LP
Note that in temporal logic, 
a fact which is true at all time must
be described using the [] operator.
Otherwise the fact is only true at present time.
.PP
Next we describe sequential circuits, such as flip-flops,
which are difficult or impossible to express using the traditional logic.
Flip-flops are expressed in the relations between the present and the next 
values of the external terminals corresponding to functional tables
such as those found in TTL handbooks.
For example, a D flip-flop, which is shown in Figure (4), is described 
in temporal logic as follows:
.IP
.nf
[](Q <-> ~ Qinv),                          (15)
[]((D/\eCk)\e/(Q/\e~Ck)) <-> \ \ Q),
[]((~D/\eCk)\e/(~Q/\e~Ck)) <-> \ \ ~Q)

(expressions marked off by a comma imply logical the conjunction)
.fi
.LP
The first expression says that the output signal Q is the inversion
of output signal Qinv, and vice versa.
The second line shows that Q is high in the next state 
iff (if and only if) the conditions in the left hand side of '<->' 
are satisfied.
The third line is interpreted in the same way.
Any flip-flop can be expressed in temporal logic using relations between
the present and the next values of terminals, which correspond to function
tables shown in TTL handbooks.
.NH 3
Timing Diagrams
.PP
Hardware designers usually use timing diagrams to clarify 
the timing relations among variables.
Temporal logic can express such relations simple, precise expressions 
such as those shown below.
.LP
For example, the handshaking sequence, shown in the Figure (5),
is described as follows.
.IP
.KS
.nf
[](Call  -> <>Hear),
[](~Hear -> ~Hear U Call),
[](~Call -> <>~Hear),
[](Hear  -> Hear U ~Call),   (16)
[](Hear  -> <>~Call),
[](Call  -> Call U Hear),
[](~Hear -> <>Call),
[](~Call -> ~Call U ~Hear)
.fi
.KE
.LP
Call is a request signal from a calling module to a called module and Hear
is a response. 
According to the the timing diagram, if Hear is low, then
Call rises; if Call rises, Hear rises; if Hear rises,
Call falls; and if Call falls, Hear falls. 
.PP
The 'until'
operator is  used for specifying that Call and Hear are treated
as registers.
As seen above, temporal logic can express various timing
relations and hardware specifications in the conjunction of simple
expressions.
.PP
More complex examples, such as that shown in Figure Figure (6-a): 'During 
the period from the time when the start signal S1 is active
till the time when the end signal E1 is active,
if P is active, then Q is active on the next time'
is described as
.IP
[](S1 -> ((P -> o Q) U E1))   (17)
.LP
(17) assumes that S and E are provided externally as pulses
like in Figure (6-a).
.LP
This is shown in temporal logic as follows.
.IP
.nf
[](S1 -> ((o ~S1)) U E1)),
(o ~E1) U S1,                 (18)
[](E1 -> ((o ~E1) U S1))  )
.fi
.PP
Moreover, as seen in Figure (6-b), a more complex relation: 'During
the period from the time when the start signal S2 is active
till the time when the end signal E2 is active during
the period from the time when the start signal S1 is active
till the time when the end signal E1 is active,
if P is active, then Q is active on the next time'
is described as
.IP
 [](S1 -> ((S2 -> ((P -> \ \ Q)) U E2)) U E1))   (19)
.PP
As seen from (17) and (18), complex specifications require multiply nested
temporal operators.
However, consider an interval I1 and I2 are introduced
as follows.
I1 is active during the period from 
the time when S1 is active till the time when E1 is active, and 
inactive during the period from the time when E1 is active 
till the time when S1 is active.
And another interval 
I2 is active during the period where I1 is active and
from the time when S2 is active till the time when E2 is active, 
and inactive during the period where I1 is inactive or from 
the time when E1 is active.
The specification (19) (and also (17)) is described with the conjunction of
the following simple expressions. See Figure (7).
.KS
.IP
.nf
[](~I1 -> ((~I1) U S1)))
[](S1 -> I1)
[](I1 -> (I1 U E1))                    (20)
[](E1 -> (~I1))
[](~I2 -> ((~I2) U (S2/\eI1))))
[]((S2/\eI1) -> I2)
[](I2 -> (I2 U (E2/\eI1)))
[]((E2/\eI1) -> (~I2))
[]((I2/\eP) -> o Q)
.fi
.KE
.LP
The first four expressions guarantee that I1 is active only
in the period from the time when S1 is active till the time when 
E1 is active. 
The following four expressions guarantee that I2 is active only
in the period where I1 is active and from the time when S2 
is active till the time when 
E2 is active. 
The last expression means that whenever I2 is active,
if P is active, Q is active on the next state.
.PP
As a rule, by introducing interval variables like I1 and  I2,
complex specifications can be described
as the conjunction of simple expressions.
Although interval variables I1 and  I2  specify internal state, 
which are not observable from the outside, 
such interval variables simplify module specification.
Also, as there are many expressions of the same type as seen in (20),
the time required for the verification and synthesis of complex specifications
for synchronization parts is kept manageably small
as described in [11,12,13].
The next section describes a basic technique
for describing hardware behaviors 
in LTTL and interval.
In chapter 3 and 4, we introduce a logic
programming language, Tokio.
.NH 2
Behavior Descriptions Using Intervals
.PP
Elegant description of hardware behavior demands a capability of
no only declarative descriptions, but procedural descriptions as well.
There are two aspects of 
Procedural descriptions : parallel and sequential.
It is easy to describe parallelisms in temporal logic.
Parallelisms are described simply as the conjunction of each action.
For example, 'the two actions: P-> o Q and R-> o S are working 
in parallel' is described as 
.IP
 (P-> o Q)/\e(R-> o S).      (21)
.PP
However, it is tedious and not difficult to describe sequentiality.
For example, when we attempt to describe 
'first execute P and then
execute Q' in PASCAL,
.IP
 begin
   P;
   Q      (22)
 end
.LP
the following things must be specified.
.IP
.nf
 first P is executed.
 All the time when P is executed, Q is not executed.
 If P is ended, then Q is started to execute.         (23)
 All the time when Q is executed, P is not executed. 
.fi
.PP
If we use signals indicating whether P and Q are executed or not,
the conditions above are easily described.
That is, it is very useful to introduce interval variables that are 
active only during the period when actions such as P and Q are executed,
as shown in section 2.1.3.
Let Ip and Iq be interval signals indicating execution of P and Q respectively,
and let Ip.beg and Iq.beg be variables expressing the beginning time of the
intervals and Ip.fin and Iq.fin be signals expressing the ending time
of those intervals.
Therefore, Ip.beg is active when and only when Ip rises, and Ip.fin is
active when and only when Ip falls.
Then, (23) is described as follows.
.KS
.IP
.nf
[](Ip<->P), 
[](Iq<->Q),
Ip.beg,
[](Ip.fin->Iq.beg),  (24)
[](~(Ip/\eIq))
.fi
.KE
.LP
The first two line mean that Ip and Iq indicate exactly the starting
time of the execution
of P and Q, respectively.
The third line shows that first P is active, and the fourth line shows that
if P ends, then Q begins.
The fifth line shows that P and Q are not executed at the same time.
.PP
Specification of interval variables is described as follows.
.KS
.IP
.nf
<>Ip.beg,
<>Ip.fin,
[](Ip.beg -> o ([] ~Ip.beg)),
[](Ip.fin -> o ([] ~Ip.fin)),
~Ip U o Ip.beg,                (25)
[](Ip.beg -> (Ip U Ip.fin)),
[](Ip.fin -> o ([] ~Ip))
.KE
.LP
The first four lines means 'Ip.beg and Ip.fin are unit pulses'.
The rest of the lines mean 'Ip is true during Ip.beg to Ip.fin'.
The concept of 'interval' is described in LTTL using these variables.
We describe them in Linear Time Temporal Logic only
because of the ease with which they can be manipulated.
By introducing interval variables to LTTL, ITL expressions can be translated
into LTTL.
The basic translation methods are found in [7].
.PP
Interval variables are additional variables indicating internal hardware states
that are not necessarily observable from the outside.
However, the idea of intervals makes both parallel and sequential description
much easier, as shown in the next section.
Moreover, using intervals, we can specify behaviors of hardwares in the 
conjunction of simple temporal logic expressions
like (24) and complex synchronization problems are expressed in 
propositional LTTL, which drastically reduces the time
required for synthesis and verification [11,12,13].
